/LMAR=0/XLINE=4/FONT#0=BASL30/FONT#1=BASB30/FONT#5=ASI30[LSP,JRA]/FONT#2=ASI30[LSP,JRA]/FONT#3=SUB/FONT#4=SET1/FONT#6=GRK30/FONT#7=SUP/FONT#8=SPEC[LSP,JRA]/FONT#9=BUCK75/FONT#10=GRFX25[LSP,JRA]/FONT#11=METSB/FONT#12=NGB30/FONT#13=GERM35/FONT#14=MG[LSP,JRA]/FONT#15=GRFX35
␈↓ α∂␈↓␈↓  CONTENTS␈↓ 
w␈↓








␈↓ α∂␈↓␈↓	Contents␈↓












␈↓"β␈↓ α∂␈↓␈↓ αW␈↓↓PREFACE␈↓ 
mi␈↓



␈↓"β

␈↓"β␈↓ α∂␈↓␈↓ αWTEXT
␈↓ α∂␈↓␈↓␈↓ 
@     1␈↓

␈↓"β␈↓ α∂␈↓␈↓ βS␈↓↓Practical Termination for Nondeterministic Programs␈↓
␈↓"∀␈↓ α∂␈↓Traditionally,␈αthe␈αword␈α"termination"␈αhas␈αa␈αvery␈αwell␈αunderstood␈αmeaning,␈αnamely␈α"it
␈↓ α∂␈↓stops".␈α∩ However,␈α∩one␈α∪might␈α∩consider␈α∩several␈α∪different␈α∩kinds␈α∩of␈α∪termination.␈α∩ For
␈↓ α∂␈↓example,␈α
when␈αwe␈α
speak␈α
of␈αnondeterministic␈α
languages,␈αsuch␈α
as␈α
logic,␈αthere␈α
are␈αat␈α
least
␈↓ α∂␈↓3 different ways of considering the question of termination.
␈↓"β␈↓ α∂␈↓␈↓ αWThe␈α"safe"␈αinterpretation␈αof␈αtermination␈αin␈αthe␈αpresence␈αof␈αnondeterminism␈αis␈αto
␈↓ α∂␈↓say:␈α⊂a␈α⊂program␈α∂always␈α⊂"terminates"␈α⊂if␈α∂and␈α⊂only␈α⊂if␈α∂every␈α⊂possible␈α⊂computation␈α∂path
␈↓ α∂␈↓terminates.␈α⊂This␈α∂is␈α⊂the␈α∂most␈α⊂common␈α⊂interpretation,␈α∂but␈α⊂it␈α∂may␈α⊂be␈α⊂more␈α∂restrictive
␈↓ α∂␈↓than␈αnecessary.␈α
 At␈αthe␈α
other␈αextreme␈α
we␈αcould␈α
say␈αthe␈α
program␈α"terminates"␈α
if␈αthere
␈↓ α∂␈↓exists␈α
a␈αcomputation␈α
path␈αwhich␈α
terminates.␈α
 This␈αinterpretation␈α
is␈αsufficient␈α
if␈αwe␈α
can
␈↓ α∂␈↓always␈αfind␈αthe␈αappropriate␈αpath␈αfor␈αeach␈αcomputation.␈α A␈αthird␈αinterpretation␈αis␈αone
␈↓ α∂␈↓in␈α∪which␈α∪we␈α∪say␈α∪that␈α∪a␈α∀program␈α∪always␈α∪terminates␈α∪with␈α∪respect␈α∪to␈α∀a␈α∪particular
␈↓ α∂␈↓interpreter,␈αor␈α
a␈αparticular␈αevaluation␈α
strategy.␈α We␈αall␈α
know␈αthat␈αthere␈α
are␈αprograms
␈↓ α∂␈↓which␈α∂will␈α∂terminate␈α∂under␈α∂call-by-name␈α∞evaluation␈α∂and␈α∂not␈α∂under␈α∂call-by-value␈α∞(in
␈↓ α∂␈↓the␈αpresence␈αof␈αside␈αeffects,␈αthe␈αreverse␈αis␈αalso␈αtrue).␈α If␈αwe␈αuse␈αa␈αbreadth␈αfirst␈αsearch,
␈↓ α∂␈↓or␈α∂computation␈α∂strategy,␈α∂(that␈α∂is,␈α∂follow␈α∂all␈α∞paths␈α∂in␈α∂parallel)␈α∂we␈α∂know␈α∂that␈α∂we␈α∞will
␈↓ α∂␈↓always␈αbe␈αable␈αto␈αdiscover␈αa␈αterminating␈αcomputation␈αif␈αany␈αexists.␈α However,␈αthis␈αcan
␈↓ α∂␈↓be␈α∞extremely␈α∞costly␈α∞in␈α
both␈α∞time␈α∞and␈α∞space,␈α∞and␈α
is␈α∞not␈α∞usually␈α∞necessary.␈α∞ Using␈α
the
␈↓ α∂␈↓"safe"␈α∀definition␈α∀of␈α∪termination,␈α∀the␈α∀computation␈α∪rule␈α∀used␈α∀makes␈α∀no␈α∪difference;
␈↓ α∂␈↓however,␈α⊃we␈α⊃restrict␈α⊃ourselves␈α⊃unnecessarily␈α⊃from␈α⊃considering␈α⊃programs␈α⊃which␈α⊂will
␈↓ α∂␈↓always terminate under the conditions in which we intend to use them.
␈↓"β␈↓ α∂␈↓␈↓ αWWe␈α∀intend␈α∀to␈α∀consider␈α∀termination␈α∀in␈α∀a␈α∀pragmatic␈α∀way.␈α∀ Our␈α∀treatment␈α∀is
␈↓ α∂␈↓informal␈α
and␈α∞intended␈α
to␈α∞make␈α
some␈α∞useful␈α
special␈α∞cases␈α
obvious␈α∞to␈α
the␈α∞novice␈α
who
␈↓ α∂␈↓finds␈α
the␈αsubject␈α
of␈αproving␈α
termination␈αof␈α
programs␈αprohibitively␈α
complicated␈αat␈α
first
␈↓ α∂␈↓glance␈αand␈αis␈α
thus␈αdiscouraged␈αfrom␈α
the␈αendeavor␈αentirely.␈α
 We␈αshall␈αdescribe␈αa␈α
useful
␈↓ α∂␈↓class␈α⊂of␈α⊂programs,␈α⊂guaranteed␈α⊂to␈α⊂terminate␈α⊂given␈α⊂certain␈α⊂restrictions␈α⊂on␈α⊃the␈α⊂calling
␈↓ α∂␈↓style.␈α Since␈αwe␈αwill␈αbe␈αdealing␈α
with␈αlogic␈αprograms␈α(partially␈αcorrect␈αby␈αdefinition),␈α
we
␈↓ α∂␈↓will have totally correct programs.
␈↓"β␈↓ α∂␈↓␈↓ αWA␈αlogic␈α
program␈αis␈α
a␈αset␈α
of␈αHorn␈α
clauses,␈αeach␈α
of␈αwhich␈α
is␈αan␈α
implication␈αwith␈α
at
␈↓ α∂␈↓most one consequent.  For example,
␈↓"β␈↓ α∂␈↓␈↓ ¬ ␈↓A ← B␈↓β1␈↓ ∧ B␈↓β2␈↓ ∧ ... ∧ B␈↓βn␈↓
␈↓"β␈↓ α∂␈↓␈↓ αWThe␈α⊂procedural␈α∂interpretation␈α⊂of␈α∂a␈α⊂Horn␈α∂clause␈α⊂is␈α∂as␈α⊂a␈α⊂procedure␈α∂declaration
␈↓ α∂␈↓[Kowalski,␈α1973].␈α The␈αconsequent,␈α
␈↓A␈↓,␈αis␈αthe␈αprocedure␈α
name␈αand␈αthe␈αlist␈α
of␈αsubgoals
␈↓ α∂␈↓␈↓B␈↓β1␈↓,␈α
...,␈α∞B␈↓βn␈↓␈α
make␈α∞up␈α
the␈α∞procedure␈α
body.␈α
 A␈α∞clause␈α
with␈α∞an␈α
empty␈α∞list␈α
of␈α∞subgoals␈α
is
␈↓ α∂␈↓thus␈α
a␈α
procedure␈α∞with␈α
no␈α
body␈α∞and␈α
is␈α
taken␈α
to␈α∞be␈α
an␈α
assertion␈α∞of␈α
fact.␈α
 A␈α∞clause␈α
in
␈↓ α∂␈↓which the procedure name is missing, for example
␈↓"β␈↓ α∂␈↓␈↓ ¬X␈↓← B␈↓β1␈↓ ∧ ... ∧ B␈↓βn␈↓
␈↓"β␈↓ α∂␈↓␈↓ αWis taken to be a nameless procedure or simply a sequence of goals to be satisfied.
␈↓"β␈↓ α∂␈↓␈↓ αWA␈α∞logic␈α∞program␈α
is␈α∞an␈α∞assertional␈α∞specification␈α
of␈α∞the␈α∞relationships␈α∞which␈α
hold
␈↓ α∂␈↓among␈α∂the␈α∂objects␈α∂it␈α∂operates␈α∂on.␈α∂ It␈α∞is␈α∂a␈α∂statement␈α∂of␈α∂its␈α∂own␈α∂axiomatic␈α∞semantics.
␈↓ α∂␈↓However,␈αwe␈αdo␈αnot␈αwish␈αto␈αconsider␈αhere␈αall␈αsyntactically␈αcorrect␈αlogic␈αprograms,␈αbut
␈↓ α∂␈↓only␈α⊂those␈α⊂which␈α⊂are␈α⊂"computational",␈α⊂that␈α⊂is,␈α⊂programs␈α⊂whose␈α⊂computation␈α⊂is␈α∂well
␈↓ α∂␈↓spelled␈α∞out.␈α∞ For␈α∞example,␈α∞a␈α∞program␈α∞may␈α∞be␈α∞driven␈α∞by␈α∞the␈α∞structure␈α∞of␈α∞the␈α∞data␈α∞it
␈↓ α∂␈↓operates on, decomposing that structure until a basis case is reached.
␈↓ α∂␈↓␈↓2  ␈↓ 
w␈↓

␈↓"β␈↓ α∂␈↓␈↓ αWThis␈αof␈αcourse␈αrequires␈αthat␈αwe␈αknow␈αwhich␈αof␈αthe␈αarguments␈αto␈αa␈αpredicate␈αare
␈↓ α∂␈↓intended␈αto␈α
provide␈αinput,␈αthe␈α
computation␈αbeing␈αbased␈α
on␈αthe␈αdecomposition␈α
of␈αone
␈↓ α∂␈↓or␈αmore␈αof␈αthese␈α
arguments␈αto␈αa␈αbasis␈α
case␈αor␈αperhaps,␈αas␈α
in␈αthe␈αcase␈αof␈α
real␈αnumber
␈↓ α∂␈↓algorithms, based on reaching some acceptable error tolerance.
␈↓"β␈↓ α∂␈↓␈↓ αWGiven␈α⊂the␈α⊂restriction␈α⊂that␈α∂we␈α⊂will␈α⊂always␈α⊂specify␈α∂which␈α⊂of␈α⊂the␈α⊂arguments␈α∂are
␈↓ α∂␈↓intended␈α∀to␈α∀be␈α∀input␈α∪and␈α∀which␈α∀are␈α∀intended␈α∪to␈α∀hold␈α∀the␈α∀answer,␈α∀we␈α∪consider
␈↓ α∂␈↓termination␈α∞with␈α∂respect␈α∞to␈α∂these␈α∞conventions.␈α∂ For␈α∞example,␈α∂a␈α∞logic␈α∂program␈α∞which
␈↓ α∂␈↓computes the greatest common divisor of two given natural numbers is as follows:

␈↓"β␈↓ α∂␈↓␈↓ αW        GCD(0,x,x) ←

␈↓"β␈↓ α∂␈↓␈↓ αW        GCD(x,0,x) ←

␈↓"β␈↓ α∂␈↓␈↓ αW        GCD(x,y,z) ← ␈↓≤␈↓(x,y) ∧ GCD(x,y-x,z) ∧ Nat(x) ∧ Nat(y-x)

␈↓"β␈↓ α∂␈↓␈↓ αW        GCD(x,y,z) ← ␈↓≤␈↓(y,x) ∧ GCD(x-y,y,z) ∧ Nat(x-y) ∧ Nat(y)

␈↓"β␈↓ α∂␈↓␈↓ αWGCD(x,y,z) ␈↓means that the greatest common divisor of␈↓ x ␈↓and ␈↓y ␈↓is␈↓ z.
␈↓"β␈↓ α∂␈↓␈↓ αW␈↓≤␈↓(x,y)␈↓ means that ␈↓x␈↓ is less than or equal to ␈↓y.
␈↓"β␈↓ α∂␈↓␈↓ αWNat(x) ␈↓means that ␈↓x␈↓ is a natural number.

␈↓"β␈↓ α∂␈↓␈↓ αW The␈α⊃logic␈α⊃program␈α⊂␈↓GCD␈↓␈α⊃is␈α⊃easily␈α⊂shown␈α⊃to␈α⊃terminate␈α⊂as␈α⊃long␈α⊃as␈α⊃we␈α⊂always
␈↓ α∂␈↓provide␈α
the␈α
natural␈α
numbers␈α
␈↓x␈↓␈α
and␈α∞␈↓y␈↓␈α
as␈α
input␈α
and␈α
expect␈α
to␈α
compute␈α∞their␈α
greatest
␈↓ α∂␈↓common␈αdivisor␈α
in␈α␈↓z␈↓.␈α
 If␈αhowever,␈α
we␈αwere␈α
to␈αprovide␈α
natural␈αnumbers␈α
for␈α␈↓x␈↓␈α
and␈α␈↓z␈↓,
␈↓ α∂␈↓asking␈α
in␈α
effect␈α∞for␈α
␈↓y␈↓,␈α
a␈α∞number␈α
such␈α
that␈α
the␈α∞␈↓GCD(x,y,z)␈↓,␈α
the␈α
program␈α∞may␈α
never
␈↓ α∂␈↓terminate.␈α
 If␈α
␈↓z␈↓␈α∞does␈α
not␈α
divide␈α∞␈↓x␈↓␈α
then␈α
we␈α
can␈α∞never␈α
find␈α
an␈α∞answer,␈α
and␈α
if␈α∞␈↓z␈↓␈α
does
␈↓ α∂␈↓divide␈α
␈↓x␈↓,␈α
then␈α
there␈α
are␈α
an␈α
infinite␈α
number␈α
of␈α
answers.␈α
 Thus,␈α
if␈α
we␈α
are␈α
to␈α
compute␈α
all
␈↓ α∂␈↓of␈α⊃them,␈α∩we␈α⊃will␈α⊃never␈α∩terminate.␈α⊃ Furthermore,␈α⊃if␈α∩we␈α⊃are␈α⊃content␈α∩to␈α⊃stop␈α∩at␈α⊃one
␈↓ α∂␈↓answer,␈α∞it␈α∞may␈α∞be␈α∞a␈α∞different␈α∞one␈α∞every␈α∞time␈α∞the␈α∞program␈α∞is␈α∞run,␈α∞since␈α∞we␈α∞have␈α
no
␈↓ α∂␈↓indication␈αin␈α
the␈αprogram␈αof␈α
how␈αto␈α
generate␈αpossible␈α␈↓y␈↓␈α
values.␈α Without␈αknowing␈α
the
␈↓ α∂␈↓internal␈α∞workings␈α∂of␈α∞the␈α∂interpreter␈α∞we␈α∂can't␈α∞tell␈α∞how␈α∂this␈α∞may␈α∂be␈α∞done.␈α∂ Thus,␈α∞the
␈↓ α∂␈↓␈↓GCD␈↓␈α
program␈α
is␈α
considered␈α
"computational"␈α
only␈α
given␈α
the␈α
restriction␈α
that␈α
x␈α
and␈α
y␈α
are
␈↓ α∂␈↓to be input values and z an output value.
␈↓"β␈↓ α∂␈↓␈↓ αWThis␈α⊃approach␈α⊃does␈α⊃not␈α⊃profit␈α⊃from␈α⊃the␈α⊃generality␈α⊃of␈α⊃logic␈α⊃programs,␈α⊃which
␈↓ α∂␈↓express␈α∞relationships␈α∞among␈α∞arguments␈α
rather␈α∞than␈α∞simply␈α∞supply␈α∞output.␈α
 However,
␈↓ α∂␈↓we␈α
contend␈α
that␈α
most␈α
programs␈α
are␈α
written␈α
with␈α
the␈α
intent␈α
of␈α
providing␈α
answers␈α
which
␈↓ α∂␈↓are␈α⊃functions␈α⊃of␈α⊂some␈α⊃input.␈α⊃ We␈α⊂usually␈α⊃know␈α⊃which␈α⊂information␈α⊃is␈α⊃going␈α⊃to␈α⊂be
␈↓ α∂␈↓available␈αand␈αwhich␈αis␈α
to␈αbe␈αcomputed.␈↓π 1␈↓␈αWe␈α
base␈αour␈αalgorithms␈αon␈α
this␈αknowledge.
␈↓ α∂␈↓When␈αwe␈αare␈αcomputing␈αa␈αfunction␈αof␈αsome␈αarguments␈αwe␈αknow␈αthat␈αthere␈α
is␈αexactly

␈↓"β␈↓ α∂␈↓________________
␈↓"β␈↓ α∂␈↓␈↓ αW␈↓π 1␈↓The␈α∩notable␈α∩exception␈α∩to␈α∩this␈α∩generalization␈α∩is␈α∩data␈α∩base␈α∩handling.␈α⊃ Logic
␈↓ α∂␈↓programs␈α⊂are␈α⊂naturals␈α⊂for␈α⊂this␈α⊂kind␈α⊂of␈α⊂application,␈α⊂expressing␈α⊂relationships␈α∂among
␈↓ α∂␈↓elements␈α
of␈αthe␈α
data␈αbase␈α
and␈α
being␈αcapable␈α
of␈αretrieving␈α
information␈αon␈α
any␈α
of␈αthe
␈↓ α∂␈↓missing arguments.  See [van Emden] for this type application.
␈↓ α∂␈↓␈↓␈↓ 
@     3␈↓

␈↓"β␈↓ α∂␈↓one␈α∩answer.␈α∩ However,␈α∩a␈α∩well-defined␈α∩function␈α∩may␈α∩map␈α∩several␈α∩different␈α∩sets␈α∩of
␈↓ α∂␈↓arguments␈αin␈αits␈αdomain␈αto␈αthe␈αsame␈αvalue␈αin␈αits␈αrange,␈αdestroying␈αthe␈αfunctionality␈α
of
␈↓ α∂␈↓the␈α⊃inverse␈α⊃operation,␈α⊃as␈α⊃in␈α⊂the␈α⊃example␈α⊃above.␈α⊃ We␈α⊃consider␈α⊃computational␈α⊂logic
␈↓ α∂␈↓programs␈αto␈αbe␈αthose␈αin␈αwhich␈αthe␈αcomputation␈αis␈αdriven␈αin␈αsuch␈αa␈αway␈αas␈αto␈αsimplify
␈↓ α∂␈↓each␈αrecursive␈αcall␈αin␈αthe␈αsense␈αof␈αgetting␈αcloser␈αto␈αthe␈αbasis␈αor␈αtermination␈αclauses␈αof
␈↓ α∂␈↓the␈αprogram.␈α Not␈α
only␈αdoes␈αthis␈α
simplification␈αhave␈αto␈αhappen␈α
but␈αit␈αhas␈α
to␈αhappen
␈↓ α∂␈↓"fast␈αenough".␈α
 That␈αis,␈α
we␈αmust␈α
be␈αconvinced␈αthat␈α
we␈αcannot␈α
have␈αan␈α
infinite␈αchain
␈↓ α∂␈↓of␈αsimplifications␈α
between␈αthe␈αcase␈α
at␈αhand␈αand␈α
the␈αbasis␈αcase.␈α
 This␈αcauses␈αno␈α
trouble
␈↓ α∂␈↓if␈α⊃we␈α∩are␈α⊃using␈α∩inductively␈α⊃defined␈α∩data␈α⊃structures,␈α∩since␈α⊃there␈α∩is␈α⊃always␈α∩a␈α⊃finite
␈↓ α∂␈↓number␈α
of␈α
applications␈αof␈α
constructors␈α
to␈αbasis␈α
elements␈α
which␈αmake␈α
up␈α
any␈αelement
␈↓ α∂␈↓of␈α
the␈α
data␈α∞structure.␈α
 However,␈α
in␈α∞the␈α
case␈α
of␈α
real␈α∞number␈α
algorithms,␈α
we␈α∞have␈α
the
␈↓ α∂␈↓additional␈α
problem␈α
of␈αshowing␈α
that␈α
we␈αreduce␈α
the␈α
problem␈αfast␈α
enough␈α
to␈α
reach␈αour
␈↓ α∂␈↓tolerance␈αof␈αerror.␈αSee␈α[Clark,␈αMcKeeman,␈αSickel,␈α1978].␈α Here␈αwe␈αsimplify␈αmatters␈αby
␈↓ α∂␈↓considering only programs which operate on inductively definable domains.
␈↓"β␈↓ α∂␈↓␈↓ αWFor␈α
logic␈αprograms␈α
which␈α
are␈αcomputational␈α
in␈α
the␈αsense␈α
described␈α
above␈αwe␈α
can
␈↓ α∂␈↓speak␈α⊂of␈α∂termination␈α⊂in␈α∂a␈α⊂pragmatic␈α∂way.␈α⊂ We␈α∂specify␈α⊂which␈α∂parameters␈α⊂are␈α⊂to␈α∂be
␈↓ α∂␈↓input␈α∪and␈α∪which␈α∪are␈α∪to␈α∀be␈α∪output,␈α∪and␈α∪guarantee␈α∪termination␈α∪only␈α∀under␈α∪these
␈↓ α∂␈↓restrictions.
␈↓"β␈↓ α∂␈↓␈↓ αWThe␈α∞decomposition␈α∞of␈α
the␈α∞input␈α∞values␈α∞in␈α
a␈α∞computational␈α∞logic␈α∞program␈α
need
␈↓ α∂␈↓not␈α∪be␈α∪an␈α∪explicit␈α∪stripping␈α∪of␈α∩constructor␈α∪functions.␈α∪ For␈α∪example,␈α∪in␈α∪the␈α∩␈↓GCD␈↓
␈↓ α∂␈↓program,␈α∩we␈α∪do␈α∩not␈α∪intend␈α∩to␈α∪represent␈α∩every␈α∪natural␈α∩number␈α∪as␈α∩a␈α∪sequence␈α∩of
␈↓ α∂␈↓applications␈αof␈α"successor"␈αto␈α"0".␈α We␈αinclude␈αas␈αa␈αsubgoal␈αthe␈αresrtriction␈αthat␈αwe␈αare
␈↓ α∂␈↓at␈αeach␈αstep␈αstil␈αdealing␈αwith␈αnatural␈αnumbers.␈α
 This␈αallows␈αus␈αto␈αuse␈αthe␈αbuilt␈αin␈α
data
␈↓ α∂␈↓types␈α∩of␈α∩the␈α∩machine␈α∩we␈α∩are␈α∩using␈α∩and␈α∩to␈α∩define␈α∩others␈α∩in␈α∩terms␈α∩of␈α∩them.␈α∩ For
␈↓ α∂␈↓example,␈αif␈αa␈αtype␈α"integer"␈αis␈αavailable,␈αit␈αis␈αmore␈αconvenient␈αto␈αdefine␈α␈↓Nat(x)␈↓,"␈↓x␈↓␈αis␈α
a
␈↓ α∂␈↓natural␈α∞number",␈α∞as␈α∞"␈↓x␈↓␈α∞is␈α∞an␈α∞integer␈α∞grater␈α∞than␈α∞or␈α∞equal␈α∞to␈α∞0",␈α∞and␈α∞be␈α∞able␈α∞to␈α
use
␈↓ α∂␈↓built␈αin␈αinteger␈α
arithmetic,␈αrather␈αthan␈α
define␈αnatural␈αnumbers␈α
inductively␈αfrom␈α0␈α
and
␈↓ α∂␈↓successor and redefine all arithmetic functions to operate on them appropriately.
␈↓"β␈↓ α∂␈↓Theorem

␈↓"β␈↓ α∂␈↓Let␈α␈↓P␈↓␈αbe␈αa␈αrecursive␈αprogram␈α
which␈αoperates␈αon␈αan␈αinductively␈αdefined␈αdata␈α
structure
␈↓ α∂␈↓␈↓D␈↓␈α∂(one␈α∂for␈α∂which␈α∞it␈α∂is␈α∂possible␈α∂to␈α∞give␈α∂an␈α∂inductive␈α∂definition).␈α∞Let␈α∂␈↓x␈↓␈α∂be␈α∂a␈α∞formal
␈↓ α∂␈↓parameter to ␈↓P␈↓.  Then, ␈↓P␈↓ will terminate if
␈↓"β␈↓ α∂␈↓        1)  The termination, or basis, clause of ␈↓P␈↓ is applicable if ␈↓x␈↓ is
␈↓"β␈↓ α∂␈↓bound to any basis element of ␈↓D␈↓; and
␈↓"β␈↓ α∂␈↓        2)  The value of ␈↓x␈↓ is simplified, or decomposed, with every
␈↓"β␈↓ α∂␈↓recursive call to the program; and
␈↓"β␈↓ α∂␈↓        3)  There are no non-terminating subgoals.

␈↓"β␈↓ α∂␈↓proof:␈α
by␈α
induction␈α
on␈α
the␈α
number␈α
of␈α
applications␈α
of␈α
the␈α
constructor␈α
function␈α
involved
␈↓ α∂␈↓in␈α⊂the␈α⊂value␈α⊃of␈α⊂␈↓x␈↓.␈α⊂ Since␈α⊃by␈α⊂2)␈α⊂␈↓x␈↓␈α⊃is␈α⊂decomposed␈α⊂in␈α⊃every␈α⊂recursive␈α⊂call,␈α⊃the␈α⊂only
␈↓ α∂␈↓applicable␈αclause␈αwill␈αbe␈αa␈αtermination␈αclause␈αwhen␈α␈↓x␈↓␈αis␈αa␈αbasis␈αelement.␈α(i.e.␈αit␈αwill␈αbe
␈↓ α∂␈↓impossible to further decompose ␈↓x␈↓ so no recursive call will be applicable)
␈↓ α∂␈↓␈↓4  ␈↓ 
w␈↓

␈↓"β␈↓ α∂␈↓␈↓ αWThe␈α
third␈αcondition␈α
of␈αthe␈α
theorem␈α
implies␈αthat␈α
we␈αare␈α
building␈α
up␈αdefinitions
␈↓ α∂␈↓of␈αprograms␈αfrom␈αothers␈α
which␈αare␈αknown␈αto␈αterminate.␈α
 It␈αis␈αreasonable␈αto␈αassume␈α
we
␈↓ α∂␈↓are␈α
given␈αcertain␈α
primitive␈αprograms␈α
which␈α
are␈αguaranteed␈α
to␈αterminate␈α
with␈αwhich␈α
to
␈↓ α∂␈↓build␈α⊂more␈α⊂complex␈α⊂programs.␈α⊂ We␈α⊂wish␈α⊂to␈α⊂have␈α⊂confidence␈α⊂that␈α⊂we␈α⊂can␈α∂combine
␈↓ α∂␈↓correct␈αcomponents␈αis␈αsuch␈αa␈αway␈αas␈αto␈αguarantee␈αcorrectness.␈α One␈αcan␈αensure␈αproper
␈↓ α∂␈↓termination␈αfor␈αone's␈αlogic␈αprograms␈αwhile␈αmaking␈αfull␈αuse␈αof␈αthe␈αtools␈αat␈αhand.␈α The
␈↓ α∂␈↓rules to remember are:

␈↓"β␈↓ α∂␈↓1) Specify which are input and which are output variables.

␈↓"β␈↓ α∂␈↓2)␈αInsure␈α
that␈αthe␈α
termination␈αcase␈α
is␈αall␈αthat␈α
is␈αapplicable␈α
when␈αa␈α
basis␈αelement␈αof␈α
the
␈↓ α∂␈↓data structure is operated on.

␈↓"β␈↓ α∂␈↓3)␈α∞Each␈α∞recursive␈α∞call␈α∂must␈α∞simplify␈α∞some␈α∞designated␈α∂input␈α∞variable␈α∞in␈α∞the␈α∂sense␈α∞of
␈↓ α∂␈↓bringing it closer to the basis element(s) of the domain.

␈↓"β␈↓ α∂␈↓␈↓ αWThe␈α∞decomposition␈α∞of␈α∂the␈α∞data␈α∞structure␈α∞must␈α∂be␈α∞done␈α∞carefully␈α∂when␈α∞making
␈↓ α∂␈↓use␈α
of␈α∞non-inductive␈α
definitions.␈α∞ For␈α
example,␈α∞in␈α
decomposing␈α∞a␈α
natural␈α∞number␈α
␈↓x␈↓,
␈↓ α∂␈↓we␈αmay␈αsimply␈αsubtract␈αone,␈αhowever,␈αwe␈αmust␈αalways␈αbe␈αsure␈αto␈αcheck␈αthat␈αthe␈αresult
␈↓ α∂␈↓is␈αindeed␈αa␈αnatural␈αnumber␈αto␈αensure␈αthat␈αwe␈αdo␈αnot␈αattempt␈αto␈α"decompose"␈αthe␈αbasis
␈↓ α∂␈↓element,␈α
"0".␈α∞ When␈α
we␈α∞have␈α
a␈α∞specific␈α
purpose␈α
in␈α∞mind␈α
it␈α∞is␈α
reasonable␈α∞to␈α
consider
␈↓ α∂␈↓the␈αproperties␈αof␈αour␈αprogram␈αwhen␈αused␈αonly␈αin␈αthe␈αway␈αintended.␈α It␈αis␈αalso␈αhelpful
␈↓ α∂␈↓to␈α
be␈αable␈α
to␈α
␈↓easily␈↓␈αconvince␈α
oneself␈αof␈α
the␈α
correctness␈αof␈α
a␈αprogram␈α
intended␈α
to␈αbe
␈↓ α∂␈↓used␈αthe␈αsame␈αway␈αat␈αall␈αtimes.␈α
 It␈αis␈αthis␈αpragmatic␈αview␈αof␈αtermination␈α
which␈αwe've
␈↓ α∂␈↓taken␈αin␈αthis␈αpaper␈αwith␈αthe␈αhope␈αof␈α
making␈αat␈αleast␈αsome␈αspecial␈αcases␈αobvious␈αto␈α
the
␈↓ α∂␈↓novice␈α
who␈α
feels␈α∞threatened␈α
by␈α
the␈α∞formal␈α
theory␈α
and␈α∞incapable␈α
of␈α
dealing␈α∞with␈α
the
␈↓ α∂␈↓general case.

␈↓"β␈↓ α∂␈↓␈↓ ¬z␈↓↓References␈↓
␈↓"∀␈↓ α∂␈↓␈↓ αWClark, K., W. McKeeman, and S. Sickel, "Logic Programming Applied to
␈↓"β␈↓ α∂␈↓␈↓ αW        Numerical Integration", 1978.
␈↓"β␈↓ α∂␈↓␈↓ αWKowalski, R., "Predicate Logic as Programming Language", Memo no. 70,
␈↓"β␈↓ α∂␈↓␈↓ αW        Edinburgh University, November, 1973.
␈↓"β␈↓ α∂␈↓␈↓ αWvan Emden, M. H., "Deductive Information Retrieval on Virtual Relational
␈↓"β␈↓ α∂␈↓␈↓ αW        Data Bases".